[TG-8293] Constant propagation for empty strings and string concatenation [blocks: #4941] #4885

danpoe · 2019-07-08T20:06:54Z

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

danpoe · 2019-07-08T20:07:52Z

src/goto-symex/symex_assign.cpp

+    {});
+
+  symbol_table_baset &st_mutable =
+    const_cast<symbol_table_baset &>(ns.get_symbol_table());


romainbrenguier

Review for the first commit

romainbrenguier · 2019-07-09T07:00:19Z

src/goto-symex/symex_assign.cpp

+#include <util/mathematical_expr.h>
+#include <util/string_expr.h>
+
+#include <iostream>


probably not necessary

romainbrenguier · 2019-07-09T07:02:06Z

src/goto-symex/symex_assign.cpp

+  const ssa_exprt &char_array,
+  const array_exprt &new_char_array)
+{
+  // assign length of string


⛏️ I find a comment like // length = new_length would be clearer

romainbrenguier · 2019-07-09T07:02:25Z

src/goto-symex/symex_assign.cpp

+    {});
+
+  symbol_table_baset &st_mutable =
+    const_cast<symbol_table_baset &>(ns.get_symbol_table());


romainbrenguier · 2019-07-09T07:03:08Z

src/goto-symex/symex_assign.h

+  bool constant_propagate_empty_string(
+    const function_application_exprt &f_l1);
+
+  void assign_constants(


🚫 documentation is missing for these two functions

romainbrenguier · 2019-07-09T07:03:55Z

src/goto-symex/symex_assign.h

-      target(target)
+      target(target),
+      char_type(16),
+      length_type(32)


these fields shouldn't be necessary and this is not language independent like symex should be.

romainbrenguier · 2019-07-09T07:23:25Z

src/goto-symex/symex_assign.cpp

+}
+
+bool symex_assignt::constant_propagate_empty_string(
+  const function_application_exprt &f_l1)


⛏️ could we use a clearer name, like function_application_l1?

romainbrenguier · 2019-07-09T07:24:24Z

src/goto-symex/symex_assign.cpp

+
+  INVARIANT(
+    f_l1.arguments().size() == 2,
+    "empty string primitive does not take arguments");


not very clear because it asserts there are 2 arguments, but the comment says there are 0

romainbrenguier · 2019-07-09T07:25:27Z

src/goto-symex/symex_assign.cpp

@@ -350,6 +358,92 @@ void symex_assignt::assign_from_struct(
  }
 }

+void symex_assignt::assign_constants(


should be made clear in the name that it is for string constants

romainbrenguier · 2019-07-09T07:29:47Z

src/goto-symex/symex_assign.cpp

+    new_char_array,
+    {});
+
+  address_of_exprt aoe(


romainbrenguier · 2019-07-09T07:31:11Z

src/goto-symex/symex_assign.cpp

+    f_l1.arguments().size() == 2,
+    "empty string primitive does not take arguments");
+
+  array_exprt char_array({}, char_array_type);


romainbrenguier · 2019-07-09T07:39:43Z

src/goto-symex/symex_assign.cpp

+  const function_application_exprt &f_l1,
+  const function_application_exprt &f_l2)
+{
+  const refined_string_exprt &s1 = to_string_expr(f_l2.arguments().at(2));


used only once, so can be inlined below. There are a lot of variables representing basically the same thing in this function (s1, s1_data_opt, s1_data) so it's bette to try to minimize that 🍋

romainbrenguier · 2019-07-09T07:44:39Z

src/goto-symex/symex_assign.cpp

+
+  const array_exprt &s1_data = s1_data_opt->get();
+
+  const refined_string_exprt &s2 = to_string_expr(f_l2.arguments().at(3));


romainbrenguier · 2019-07-09T07:44:47Z

src/goto-symex/symex_assign.cpp

+  const constant_exprt new_char_array_length =
+    from_integer(new_size, length_type);
+
+  array_typet new_char_array_type(


romainbrenguier · 2019-07-09T07:47:50Z

src/goto-symex/symex_assign.cpp

+  operands.insert(
+    operands.end(),
+    s2_data.operands().begin(),
+    s2_data.operands().end());


Ideally we should avoid duplication with the code from solver/strings/string_concatenation_builtin_function.h, concatenation is pretty simple and unlikely to change, but for functions like format we definitely need to share the code

romainbrenguier · 2019-07-09T08:08:40Z

src/goto-symex/symex_assign.cpp

+
+  array_exprt new_char_array(
+    std::move(operands),
+    new_char_array_type);


romainbrenguier · 2019-07-09T08:09:21Z

src/util/simplify_expr.h

@@ -27,4 +31,9 @@ bool simplify(
 // this is the preferred interface
 exprt simplify_expr(exprt src, const namespacet &ns);

+optionalt<std::reference_wrapper<const array_exprt>>
+try_get_string_data_array(


🚫 needs documentation

romainbrenguier · 2019-07-09T08:09:58Z

src/util/simplify_expr.h

@@ -27,4 +31,9 @@ bool simplify(
 // this is the preferred interface
 exprt simplify_expr(exprt src, const namespacet &ns);

+optionalt<std::reference_wrapper<const array_exprt>>


⛏️ optional references can be replaced by pointers

codecov-io · 2019-07-17T16:57:03Z

Codecov Report

Merging #4885 into develop will increase coverage by 0.01%.
The diff coverage is 100%.

@@             Coverage Diff             @@
##           develop    #4885      +/-   ##
===========================================
+ Coverage    69.27%   69.28%   +0.01%     
===========================================
  Files         1309     1309              
  Lines       108460   108515      +55     
===========================================
+ Hits         75133    75184      +51     
- Misses       33327    33331       +4

Impacted Files	Coverage Δ
jbmc/src/java_bytecode/java_string_literals.cpp	`94.93% <ø> (-0.42%)`	⬇️
src/util/string_utils.h	`100% <ø> (ø)`	⬆️
src/goto-symex/goto_symex.h	`92.3% <ø> (ø)`	⬆️
src/goto-symex/goto_symex.cpp	`99.15% <100%> (+2.38%)`	⬆️
src/util/simplify_expr.cpp	`87.6% <100%> (+0.33%)`	⬆️
src/util/string_utils.cpp	`93.22% <100%> (+1.06%)`	⬆️
src/solvers/strings/array_pool.cpp	`100% <100%> (ø)`	⬆️
.../strings/string_constraint_generator_constants.cpp	`63.33% <0%> (-16.67%)`	⬇️
src/util/mathematical_expr.h	`90.47% <0%> (-2.63%)`	⬇️
.../strings/string_concatenation_builtin_function.cpp	`84.09% <0%> (-2.28%)`	⬇️
... and 17 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update d4e0bd0...d9f75eb. Read the comment docs.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 19f8245).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/119510875

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 686dd8a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/120002129
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: d0b5245).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/120004102

…space Create auxiliary symbols with a different name than symbols in namespace [blocks: #4885]

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 71d11d5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/121745220

romainbrenguier · 2019-08-06T12:23:30Z

src/goto-symex/goto_symex.cpp

+  const auto &ibv_type =
+    to_integer_bitvector_type(to_array_type(char_array.type()).subtype());
+
+  const std::size_t n_bits = ibv_type.get_width();


⛏️ ibv_type is used only once, it can be inlined here since the variable name doesn't give any information.

Does provide information, and is more readable as is imo

I wouldn't know what ibv meant if it wasn't followed by to_integer_bitvector_type, so at least to me it gives no information

romainbrenguier · 2019-08-06T12:25:37Z

src/goto-symex/goto_symex.cpp

+  return new_aux_symbol;
+}
+
+void goto_symext::associate_array_to_pointer(


ns can be given as an argument

romainbrenguier · 2019-08-06T12:26:23Z

src/goto-symex/goto_symex.cpp

+    ns,
+    state.symbol_table);
+
+  ssa_exprt ssa_expr(return_symbol.symbol_expr());


romainbrenguier · 2019-08-06T12:26:32Z

src/goto-symex/goto_symex.cpp

+  function_application_exprt array_to_pointer_app(
+    function_symbol.symbol_expr(), {new_char_array, string_data});
+
+  symbolt &return_symbol = get_fresh_aux_symbol(


romainbrenguier · 2019-08-06T12:26:56Z

src/goto-symex/goto_symex.cpp

+  const symbolt &function_symbol =
+    ns.lookup(ID_cprover_associate_array_to_pointer_func);
+
+  function_application_exprt array_to_pointer_app(


const and { } initialization is prefered

romainbrenguier · 2019-08-06T12:30:57Z

src/goto-symex/goto_symex.cpp

+    aux_symbol.value == new_char_array,
+    "symbol shall have value derived from char array content");
+
+  address_of_exprt string_data(


romainbrenguier · 2019-08-06T12:34:07Z

src/goto-symex/goto_symex.cpp

+  return false;
+}
+
+void goto_symext::assign_string_constant(


I don't think this function belongs in the goto_symext class, it doesn't seem to use any of its field (apart from ns which could be given as argument). 🐙

romainbrenguier · 2019-08-06T12:34:19Z

src/goto-symex/goto_symex.cpp

+  }
+}
+
+const symbolt &goto_symext::get_new_string_data_symbol(


romainbrenguier · 2019-08-06T12:35:07Z

src/goto-symex/goto_symex.cpp

+  return try_get_string_data_array(s_pointer_opt->get(), ns);
+}
+
+void goto_symext::constant_propagate_empty_string(


allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: e78d73a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/122123110
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

romainbrenguier · 2019-08-07T06:48:32Z

src/goto-symex/goto_symex.h

+  /// \param symex_assign: object handling symbol assignments
+  /// \param f_l1: application of function ID_cprover_string_empty_string_func
+  ///   with l1 renaming applied
+  void constant_propagate_empty_string(


Sorry, I forgot to ask for unit tests for this function and the one below (ideally also the others that are added to goto_symext)

I don't like the changes, but if a code owner thinks they are fine then I won't block it

danpoe · 2019-08-07T10:53:45Z

Regarding @romainbrenguier's comment above, we have agreed that adding unit tests for the added methods in goto_symext is not strictly necessary as the feature is well-tested by regression tests already. The "don't like the changes" refers to some of the added methods being members of goto_symext as opposed to being static functions (in the same file).

peterschrammel · 2019-08-07T14:53:59Z

jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation07-NonPrintableChar/Main.java

+    String s2 = "\\";
+    String s3 = s1 + s2;
+    assert s3.length() == 2;
+    assert s3.startsWith("\t");


Maybe add assert s3.endsWith("\\");

s1.equals(s2) is implemented in the models as s1.length() == s2.length() && s1.startsWith(s2) so here we're checking that the strings are equal. To keep the tests as simple as possible we're not using the models library. I don't think it's necessary to use endsWith() here as this is a test for concatenation, endsWith() is tested elsewhere.

Then it should better be assert s3.startsWith("\t\\"); if you want to emulate equals?

peterschrammel · 2019-08-07T14:56:12Z

jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/Main.java

+    StringBuilder sb = new StringBuilder();
+    String s = sb.toString();
+    assert s.isEmpty();
+    assert s.startsWith("");


Isn't that always true?

Yes it should be.

peterschrammel · 2019-08-07T14:57:46Z

jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/test.desc

+CORE
+Main.class
+--function Main.test --property "java::Main.test:()V.assertion.1" --property "java::Main.test:()V.assertion.2"
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$


Shouldn't this be exactly 1 VCC if you use --property?

--property is passed in twice here, so yes I think the value should be 2. I'll change it to use the precise value.

So it turns out that jbmc translates those assertions to something like:

if(length_return_value != 6) { assert(false); }

So if length_return_value is 6, we don't symex the assertion and thus get 0 VCCs before simplification. This is probably not stable behaviour though so I'll leave it as is. The important thing is that after simplification we have 0 remaining VCCs.

peterschrammel · 2019-08-07T15:05:32Z

src/goto-symex/goto_symex.cpp

      lhs, expr_skeletont{}, rhs, lhs_if_then_else_conditions);
  }
 }
+
+bool goto_symext::constant_propagate_assignment_with_side_effects(


but might be needed in the future

@danpoe, are there any operations where this is actually used?

peterschrammel · 2019-08-07T15:08:53Z

src/goto-symex/goto_symex.cpp

+}
+
+optionalt<std::reference_wrapper<const array_exprt>>
+goto_symext::try_evaluate_constant_string(


I prefer those methods to live in goto_symext for now as opposed to being static. The plan is to eventually create a goto_symex_constant_propagationt member of goto_symext which handles the constant propagation.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 4fecf4e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/122424687

The function is generally useful for obtaining strings that contain only alphanumeric characters.

This is so the function can be called outside of simplify_expr.cpp.

Take the content field of a refined string expression instead of taking the whole refined string expression. This will allow it to be used from the string mutators constant propagation code in goto_symex.cpp.

….cpp Previously the string solver returned an error when constant propagation of strings was used as `array_poolt::insert()` might be called for array expressions for which there is already a mapping in the `length_of_array` map.

This implements constant propagation of ID_cprover_string_concat_func and ID_cprover_string_empty_string_func which are the primitives used by StringBuilder.append(), which in turn is used to implement String concatenation using +.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: d9f75eb).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/122439299
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

danpoe requested a review from romainbrenguier July 8, 2019 20:07

danpoe commented Jul 8, 2019

View reviewed changes

romainbrenguier suggested changes Jul 9, 2019

View reviewed changes

tautschnig assigned danpoe Jul 12, 2019

danpoe force-pushed the feature/constant-propagate-string-concatenation branch from 8bd258e to 19f8245 Compare July 17, 2019 16:00

allredj reviewed Jul 17, 2019

View reviewed changes

danpoe force-pushed the feature/constant-propagate-string-concatenation branch 8 times, most recently from df38ed0 to c9c6033 Compare July 22, 2019 10:32

danpoe changed the title ~~Constant propagation for empty strings and string concatenation~~ Constant propagation for empty strings and string concatenation [depends-on: #4925] Jul 22, 2019

danpoe added the dependent - do not merge label Jul 22, 2019

danpoe force-pushed the feature/constant-propagate-string-concatenation branch from c9c6033 to 686dd8a Compare July 22, 2019 10:51

danpoe marked this pull request as ready for review July 22, 2019 10:53

danpoe requested review from kroening, martin-cs, peterschrammel, pkesseli, smowton and tautschnig as code owners July 22, 2019 10:53

danpoe force-pushed the feature/constant-propagate-string-concatenation branch from 686dd8a to d0b5245 Compare July 22, 2019 11:08

allredj reviewed Jul 22, 2019

View reviewed changes

danpoe added a commit that referenced this pull request Jul 22, 2019

Merge pull request #4925 from danpoe/feature/get-fresh-symbol-in-name…

565542d

…space Create auxiliary symbols with a different name than symbols in namespace [blocks: #4885]

allredj reviewed Aug 2, 2019

View reviewed changes

tautschnig assigned romainbrenguier Aug 4, 2019

danpoe force-pushed the feature/constant-propagate-string-concatenation branch 4 times, most recently from f363449 to 329e603 Compare August 6, 2019 11:56

romainbrenguier reviewed Aug 6, 2019

View reviewed changes

danpoe force-pushed the feature/constant-propagate-string-concatenation branch from 329e603 to e78d73a Compare August 6, 2019 13:03

allredj reviewed Aug 6, 2019

View reviewed changes

romainbrenguier reviewed Aug 7, 2019

View reviewed changes

peterschrammel reviewed Aug 7, 2019

View reviewed changes

danpoe force-pushed the feature/constant-propagate-string-concatenation branch from e78d73a to 4fecf4e Compare August 8, 2019 10:11

peterschrammel approved these changes Aug 8, 2019

View reviewed changes

allredj reviewed Aug 8, 2019

View reviewed changes

danpoe force-pushed the feature/constant-propagate-string-concatenation branch from 4fecf4e to d9f75eb Compare August 8, 2019 12:26

danpoe and others added 9 commits August 8, 2019 13:26

Move escape_non_alnum() to util/string_utils.{h,cpp}

e05c57d

The function is generally useful for obtaining strings that contain only alphanumeric characters.

Make try_get_string_data_array() non-static

36b60ef

This is so the function can be called outside of simplify_expr.cpp.

Change interface of try_get_string_data_array()

f3c5c37

Take the content field of a refined string expression instead of taking the whole refined string expression. This will allow it to be used from the string mutators constant propagation code in goto_symex.cpp.

Implement constant propagation of string concatenation

b9d5f4b

This implements constant propagation of ID_cprover_string_concat_func and ID_cprover_string_empty_string_func which are the primitives used by StringBuilder.append(), which in turn is used to implement String concatenation using +.

Add regression test that uses models-library

aff73bd

Add regression test to check verification failure

6a26848

Add regression test for 2byte char

312bba8

Add regression test for non printable character

d9f75eb

danpoe unassigned romainbrenguier Aug 8, 2019

allredj reviewed Aug 8, 2019

View reviewed changes

danpoe merged commit aa5fcda into diffblue:develop Aug 8, 2019

danpoe deleted the feature/constant-propagate-string-concatenation branch June 2, 2020 17:17


		const array_exprt &s1_data = s1_data_opt->get();

		const refined_string_exprt &s2 = to_string_expr(f_l2.arguments().at(3));

[TG-8293] Constant propagation for empty strings and string concatenation [blocks: #4941] #4885

[TG-8293] Constant propagation for empty strings and string concatenation [blocks: #4941] #4885

Conversation

danpoe commented Jul 8, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

romainbrenguier left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

romainbrenguier Jul 9, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

codecov-io commented Jul 17, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

danpoe commented Jul 8, 2019 •

edited

Loading

romainbrenguier Jul 9, 2019 •

edited

Loading

codecov-io commented Jul 17, 2019 •

edited

Loading

danpoe commented Aug 7, 2019 •

edited

Loading

danpoe Aug 7, 2019 •

edited

Loading